(set-logic ALL)
(set-info :status sat)
(set-option :produce-models true)
(set-option :sets-ext true)
(declare-fun A () (Set (_ BitVec 3)))
(declare-fun B () (Set (_ BitVec 3)))
(declare-fun universe () (Set (_ BitVec 3)))
(declare-fun x () (_ BitVec 3))
(assert (= (set.card A) 3))
(assert (= (set.card B) 3))
(assert (not (= A B)))
(assert (= (set.card (set.inter A B)) 1))
(assert (= (set.card (set.minus A B)) 2))
(assert (= (set.card (set.minus B A)) 2))
(assert (not (set.member x A)))
(assert (not (set.member x B)))
(assert (= universe (as set.universe (Set (_ BitVec 3)))))
(check-sat)

